Nuprl Lemma : Q-R-pre-preserving-conditional 11,40
es:ES, P1, P2:(E), Q1, R1, Q2, R2:(EE), dcd_P1:(e:EDec(P1(e))), f1:({e:E| P1(e)} E),
f2:({e:E| P2(e)} E).
(e, e':{e:E| P1(e)} . (Q2(f1(e),f1(e'))))
 (e, e':{e:E| P2(e)} . (Q1(f2(e),f2(e'))))
 (e:{e:E| P1(e)} , e':{e:E| P2(e)} .
 ((Q1(f1(e),f2(e')))) & ((Q1(f2(e'),f1(e)))) & ((Q2(f1(e),f2(e')))) & ((Q2(f2(e'),f1(e)))))
 f1 is Q1-R1-pre-preserving on P1
 f2 is Q2-R2-pre-preserving on P2
 [P1? f1 : f2] is Q1  Q2-R1  R2-pre-preserving on P1  P2 
latex

Definitionsx:A. B(x), , P  Q, P & Q, f is Q-R-pre-preserving on P, [P? f : g], P1  P2, t  T, P  Q, x(s), x:A. B(x), x. t(x), R1  R2, x f y, {T}, A c B, Dec(P), A, if p:P then A(p) else B fi , False
Lemmasrel or wf, Q-R-pre-preserving wf, es-E wf, not wf, decidable wf, event system wf, conditional wf2, branch wf2

origin